package core;

import java.util.LinkedList;

import symbols.Symbol;
import symbols.Symbols;

public class ProverFastPropagate extends ProverClassic {
	
	public void propagate(Node p) {
		
		LinkedList<Node> prop_queue = new LinkedList<Node>();
		prop_queue.add(p);
		while (!prop_queue.isEmpty()) {

			proverStatus.IncreasePropagateLoopCount();

			// System.out.println("propagate");
			p = prop_queue.remove();
			if (!p.status.equals(NodeStatus.sat)
					&& !p.status.equals(NodeStatus.unsat)) {
				Symbol search_for;
				Symbol opposite;
				if (p.type.equals(Symbols.and)) {
					search_for = NodeStatus.unsat;
					opposite = NodeStatus.sat;
				} else {
					if (p.type.equals(Symbols.or)) {
						search_for = NodeStatus.sat;
						opposite = NodeStatus.unsat;
					} else {
						return;
					}
				}
				boolean assign = true;
				boolean assigned = false;

				// System.out.println("childs");
				for (Node c : p.childs) {
					// System.out.println("child " + c.i + " " + c.status);
					if (c.status.equals(search_for)) {
						p.status = search_for;// opposite;
						assign = false;
						assigned = true;
						break;
					} else {
						if (!c.status.equals(opposite)) {
							assign = false;
						}
					}
				}
				if (assign == true) {
					p.status = opposite; // search_for;
					assigned = true;
				}
				
				if (assigned == true)  {
					prop_queue.addAll(p.parents);
				}		
			}
		}
	}

}
